active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
TOP1(mark1(X)) -> PROPER1(X)
ACTIVE1(f1(X)) -> ACTIVE1(X)
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
ACTIVE1(f1(X)) -> F1(active1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X1)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X2)
TOP1(ok1(X)) -> ACTIVE1(X)
IF3(ok1(X1), ok1(X2), ok1(X3)) -> IF3(X1, X2, X3)
ACTIVE1(if3(X1, X2, X3)) -> IF3(X1, active1(X2), X3)
F1(mark1(X)) -> F1(X)
ACTIVE1(f1(X)) -> IF3(X, c, f1(true))
ACTIVE1(f1(X)) -> F1(true)
PROPER1(if3(X1, X2, X3)) -> IF3(proper1(X1), proper1(X2), proper1(X3))
ACTIVE1(if3(X1, X2, X3)) -> IF3(active1(X1), X2, X3)
PROPER1(f1(X)) -> PROPER1(X)
TOP1(ok1(X)) -> TOP1(active1(X))
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X1)
F1(ok1(X)) -> F1(X)
TOP1(mark1(X)) -> TOP1(proper1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X3)
IF3(mark1(X1), X2, X3) -> IF3(X1, X2, X3)
PROPER1(f1(X)) -> F1(proper1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X2)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TOP1(mark1(X)) -> PROPER1(X)
ACTIVE1(f1(X)) -> ACTIVE1(X)
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
ACTIVE1(f1(X)) -> F1(active1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X1)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X2)
TOP1(ok1(X)) -> ACTIVE1(X)
IF3(ok1(X1), ok1(X2), ok1(X3)) -> IF3(X1, X2, X3)
ACTIVE1(if3(X1, X2, X3)) -> IF3(X1, active1(X2), X3)
F1(mark1(X)) -> F1(X)
ACTIVE1(f1(X)) -> IF3(X, c, f1(true))
ACTIVE1(f1(X)) -> F1(true)
PROPER1(if3(X1, X2, X3)) -> IF3(proper1(X1), proper1(X2), proper1(X3))
ACTIVE1(if3(X1, X2, X3)) -> IF3(active1(X1), X2, X3)
PROPER1(f1(X)) -> PROPER1(X)
TOP1(ok1(X)) -> TOP1(active1(X))
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X1)
F1(ok1(X)) -> F1(X)
TOP1(mark1(X)) -> TOP1(proper1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X3)
IF3(mark1(X1), X2, X3) -> IF3(X1, X2, X3)
PROPER1(f1(X)) -> F1(proper1(X))
PROPER1(if3(X1, X2, X3)) -> PROPER1(X2)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
IF3(mark1(X1), X2, X3) -> IF3(X1, X2, X3)
IF3(ok1(X1), ok1(X2), ok1(X3)) -> IF3(X1, X2, X3)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF3(mark1(X1), X2, X3) -> IF3(X1, X2, X3)
IF3(ok1(X1), ok1(X2), ok1(X3)) -> IF3(X1, X2, X3)
Used ordering: Polynomial interpretation [21]:
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
POL(IF3(x1, x2, x3)) = x1 + x3
POL(mark1(x1)) = 1 + x1
POL(ok1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF3(X1, mark1(X2), X3) -> IF3(X1, X2, X3)
POL(IF3(x1, x2, x3)) = x2
POL(mark1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F1(mark1(X)) -> F1(X)
F1(ok1(X)) -> F1(X)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F1(mark1(X)) -> F1(X)
F1(ok1(X)) -> F1(X)
POL(F1(x1)) = x1
POL(mark1(x1)) = 1 + x1
POL(ok1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PROPER1(f1(X)) -> PROPER1(X)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X3)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X1)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X2)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER1(f1(X)) -> PROPER1(X)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X3)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X1)
PROPER1(if3(X1, X2, X3)) -> PROPER1(X2)
POL(PROPER1(x1)) = x1
POL(f1(x1)) = 1 + x1
POL(if3(x1, x2, x3)) = 1 + x1 + x2 + x3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE1(f1(X)) -> ACTIVE1(X)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X1)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X2)
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE1(f1(X)) -> ACTIVE1(X)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X1)
ACTIVE1(if3(X1, X2, X3)) -> ACTIVE1(X2)
POL(ACTIVE1(x1)) = x1
POL(f1(x1)) = 1 + x1
POL(if3(x1, x2, x3)) = 1 + x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TOP1(ok1(X)) -> TOP1(active1(X))
TOP1(mark1(X)) -> TOP1(proper1(X))
active1(f1(X)) -> mark1(if3(X, c, f1(true)))
active1(if3(true, X, Y)) -> mark1(X)
active1(if3(false, X, Y)) -> mark1(Y)
active1(f1(X)) -> f1(active1(X))
active1(if3(X1, X2, X3)) -> if3(active1(X1), X2, X3)
active1(if3(X1, X2, X3)) -> if3(X1, active1(X2), X3)
f1(mark1(X)) -> mark1(f1(X))
if3(mark1(X1), X2, X3) -> mark1(if3(X1, X2, X3))
if3(X1, mark1(X2), X3) -> mark1(if3(X1, X2, X3))
proper1(f1(X)) -> f1(proper1(X))
proper1(if3(X1, X2, X3)) -> if3(proper1(X1), proper1(X2), proper1(X3))
proper1(c) -> ok1(c)
proper1(true) -> ok1(true)
proper1(false) -> ok1(false)
f1(ok1(X)) -> ok1(f1(X))
if3(ok1(X1), ok1(X2), ok1(X3)) -> ok1(if3(X1, X2, X3))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))